<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01//EN" "http://www.w3.org/TR/html4/strict.dtd">
<html><head>
<meta content="text/html; charset=ISO-8859-1" http-equiv="content-type"><title>help for SAToulouse</title></head>
<body>
<big><big><big><span style="font-weight: bold;">SAToulouse</span></big></big></big><br><br>This software enables to test if a set of formulas is satisfiable.<br>Ce logiciel permet de tester si un ensemble de formules est satisfiable.<br><br><br><span style="font-weight: bold;">Description of the user interface</span><br><br><img style="width: 773px; height: 491px;" alt="" src="interface_description.png"><br><br><br><br>
<span style="font-weight: bold;">
What is the syntax of the formulas in SAToulouse ?</span><br>
The syntax of formulas in SAToulouse looks like the s-expressions of the language Scheme. Here is the formal grammar:<br><br><span style="font-family: monospace;">&lt;phi&gt;,
&lt;psi&gt; ::= &lt;atomicproposition&gt; | (not &lt;phi&gt;) |
(&lt;phi&gt; or &lt;psi&gt;) | (&lt;phi&gt; and &lt;psi&gt;) | (bigand
&lt;var&gt; &lt;set&gt; &lt;phi&gt;) | (bigor &lt;var&gt; &lt;phi&gt;)
| (bigand &lt;var&gt;&nbsp;</span><span style="font-family: monospace;">&lt;set&gt;</span><span style="font-family: monospace;"> &lt;booleanexpression&gt; &lt;phi&gt;) |  (bigor &lt;var&gt;&nbsp;</span><span style="font-family: monospace;">&lt;set&gt;</span><span style="font-family: monospace;"> &lt;booleanexpression&gt; &lt;phi&gt;)</span><br style="font-family: monospace;"><br style="font-family: monospace;"><span style="font-family: monospace;">&lt;booleanexpression&gt; ::= (&lt;expression&gt; diff &lt;expression&gt;)</span><br style="font-family: monospace;"><span style="font-family: monospace;">&lt;expression&gt; ::= &lt;var&gt; | &lt;number&gt; | (&lt;expression&gt; + &lt;expression&gt;)</span><br style="font-family: monospace;"><br style="font-family: monospace;"><span style="font-family: monospace;">&lt;var&gt; ::= any symbols (example: i, j, a)</span><br><span style="font-family: monospace;">&lt;set&gt; ::= (&lt;expression&gt; .. &lt;expression&gt;) | </span><span style="font-family: monospace;">(&lt;expression&gt; </span><span style="font-family: monospace;">&lt;expression&gt; </span><span style="font-family: monospace;">&lt;expression&gt;........)</span><br style="font-family: monospace;"><span style="font-family: monospace;">&lt;number&gt; ::= 0, 1, 2, 3 etc.</span><br><span style="font-family: monospace;">&lt;atomicproposition&gt; ::= any symbols | (symbol &lt;expression&gt; &lt;expression&gt;.........)</span><br><br><br>Examples of well-formed formulas:<br><span style="font-family: monospace;">p</span><br style="font-family: monospace;"><span style="font-family: monospace;">(p and q)</span><br style="font-family: monospace;"><span style="font-family: monospace;">(p and (not q))</span><br style="font-family: monospace;"><span style="font-family: monospace;">(not p)</span><br style="font-family: monospace;"><span style="font-family: monospace;">(not (p or (not q)))</span><br style="font-family: monospace;"><span style="font-family: monospace;">(bigand i (1 2 3) (p i))</span><br style="font-family: monospace;"><span style="font-family: monospace;">(bigand i (1 .. 12) (p i))</span><br style="font-family: monospace;"><span style="font-family: monospace;">(bigand i (1 2 3) ((p i) or (q i)))</span><br style="font-family: monospace;"><span style="font-family: monospace;">(bigand i (1 .. 12) (bigor j (1 .. 10) (i diff j) ((p i) or (q j))))</span><br><br><br>Strings that are NOT well-formed formulas:<br><span style="font-family: monospace;">p and q</span><br style="font-family: monospace;"><span style="font-family: monospace;">and p q</span><br style="font-family: monospace;"><span style="font-family: monospace;">(and p q)</span><br style="font-family: monospace;"><span style="font-family: monospace;">etc.</span><br style="font-family: monospace;"><span style="font-family: monospace;">(p and not q)</span><br><br><br>
<br>
<br>
<span style="font-weight: bold;">How does SAToulouse technically work?</span><br>SAToulouse is a graphical user interface written JAVA. 
The SAT solver we use is&nbsp;<a href="http://www.sat4j.org/">SAT4J</a>.
The transformation of macros (bigand, bigor etc.) is written in Scheme
and we use Kawa. In order to display LaTEX formulas, we use <a href="http://forge.scilab.org/index.php/p/jlatexmath/">JLatexMath</a>.<br>
<br>
<br>
<br>
<br>
</body></html>